『「正しい」圏論』Taichi Uemura
上村 太一
.「正しい」圏論. 2022.
https://uemurax.github.io/notes/ctac-2022.html
圏同型
圏同値
弱圏同値
Univalent Foundations
truncation level
型の同値
f : A -> B
、
IsEquivalence f
IsEquivalence f : (y : B) -> (Contractible ((x : A) * (f x = y)))
A ≃ B : (f : A -> B) * IsEquivalence f
id-to-equiv A B : A = B -> A ≃ B
univalence A B : IsEquivalence (id-to-equiv A B)
同一視型
(identity type)
豊穣圏
Set-豊穣圏
#文献